A, B, C:MsgA. (A ||+ B)  (C ||+ A)  (C ||+ B)  (C ||+ A  B) 

latex

Definitions	t  T, P  Q, x:A. B(x), M1  M2, ma-frame-compat(A;B), P & Q, ma-frame-compatible(A;B), MsgA, M1 || M2, x:AB(x), Prop, A ||+ B
Lemmas	ma-compatible wf, ma-frame-compatible wf, msga wf, ma-join-compatible, ma-join-frame-compat, ma-join-frame-compat2